Problem:
 b(x,y) -> c(a(c(y),a(0(),x)))
 a(y,x) -> y
 a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0())

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    c1(12) -> 3*
    c1(2) -> 11*
    c1(1) -> 11*
    a1(9,2) -> 10*
    a1(11,10) -> 12*
    a1(9,1) -> 10*
    01() -> 9*
    b0(1,2) -> 3*
    b0(2,1) -> 3*
    b0(1,1) -> 3*
    b0(2,2) -> 3*
    c0(2) -> 1*
    c0(1) -> 1*
    a0(1,2) -> 4*
    a0(2,1) -> 4*
    a0(1,1) -> 4*
    a0(2,2) -> 4*
    00() -> 2*
    1 -> 4*
    2 -> 4*
    9 -> 10*
    11 -> 12*
  problem:
   
  Qed